package agent.ccs
import scala.collection.mutable.LinkedList
import cwb.Value
import cwb.Unbound
import cwb.cwb

sealed trait PrivateAgent {
  val prime = 8388593 // < 2^23
  
  def agentString: String
  
  def diverges(): Boolean
  
  def hashCode: Int
  def equals(obj: Any): Boolean
  
  protected def sxmash(factor: Int, ab: (Int, Int)): Int = {
    ab match {
      case (a,b) => {
        val n = a + factor * b // < 2^23 + 2^23 * 2^7 < 2^31
        n - prime * (n / prime) // < 2^23
        
      }
    }
  }

  
}

case class PNil() extends PrivateAgent {
  def agentString = "0"
  def diverges() = false
  
  override
  def hashCode() = 0
  
  override
  def equals(obj:Any) = {
    obj.getClass() == classOf[PNil]
  }
  
}




case class PVar(s: Symbol) extends PrivateAgent {
  val value = new Value(s)
  def agentString = value.valueOf
  
override
def hashCode() = {
  // 3 Selected arbitrarily, used to be based on the now dropped param list
 sxmash(31, (value.hashCode, 3))
 }
  
  def agent: CCSAgent = {
   cwb.dbprintln("PVAR: Getting the agent")
   CCSComponent.environment.getAgent(s) match {
     case Some(ag) => ag
     case None => throw Unbound("Agent " + s.name + " is unbound.") 
  }
  }
  
  override
  def equals(obj: Any): Boolean = {
    obj match {
      case ag: PVar => ag.asInstanceOf[PVar].s.name == s.name
      case _ => false
    }
  }

  override
  def diverges() = {
    CCSAgent.checkForBadRecursion(this)
    CCSComponent.environment.getAgent(s) match {
      case Some(ag) => true
      case None => false
    }
  }
  
}


case class PPrefix(prefixes: List[Prefix], agent: CCSAgent) extends PrivateAgent {
  override
  def hashCode() = {
    val hashes = for (p<-prefixes) yield p.hashCode()
    sxmash(37, (hashes.foldRight(37)((a,b) => sxmash(37, (a,b))), agent.hashCode()))
  }
  
  override
  def equals(obj: Any): Boolean = {
    obj match {
      case ag: PPrefix => {
        val pref = ag.asInstanceOf[PPrefix]
        pref.prefixes == prefixes && pref.agent == agent
      }
      case _ => false
    }
  }
  
  
  
  def agentString = {
    var string = ""
    prefixes foreach {
      p => string += p.prefixString() + "."
    }
    agent.privAgent match {
      case ag: PSSum => string += "(" + ag.agentString + ")"
      case ag: PParallel => string += "(" + ag.agentString + ")"
      case ag => string += ag.agentString
    }
    string
  }
  
  // Not sure why this is automatically false, but it is in the original implementation.
  override
  def diverges() = false

}

case class PSSum(agents: List[CCSAgent]) extends PrivateAgent {
  def agentString = PrivateAgent.agentListString(agents, " + ")
  
  override
  def hashCode() = {
    val hashes = for (a<-agents) yield a.hashCode()
    hashes.foldRight(11)((a,b) => sxmash(73, (a,b)))
  }
  
  override
  def equals(obj :Any): Boolean = {
    obj match {
      case sumag: PSSum => sumag.asInstanceOf[PSSum].agents == agents
      case _ => false
    }
  }
  
  override
  def diverges(): Boolean = {
    // If we find an agent that diverges immediately return.
    for (ag <- agents) {
      if (ag.diverges()) return true
    }
    false
  }
}


case class PParallel(agents: List[CCSAgent]) extends PrivateAgent {
  def agentString = PrivateAgent.agentListString(agents, " | ")
  
  override
  def hashCode() = {
    val hashes = for (a<-agents) yield a.hashCode()
    hashes.foldRight(13)((a,b) => sxmash(13, (a,b)))
  }
  
  override
  def equals(obj: Any): Boolean = {
    obj match {
      case ag: PParallel => {
        ag.asInstanceOf[PParallel].agents == agents
      }
      case _ => false
    }
  }
  
  
  def diverges(): Boolean = {
    for (ag <- agents) {
      if (ag.diverges()) return true
    }
    false
  }
}


case class PRestrict(agent: CCSAgent, restriction: Restriction) extends PrivateAgent {
  def agentString = {
    agent.privAgent match {
      case ag: PParallel => "(" + ag.agentString + ")\\" + restriction.restrictionString
      case ag: PPrefix => "(" + ag.agentString + ")\\" + restriction.restrictionString
      case ag => ag.agentString + "\\" + restriction.restrictionString
    }
  }
  
  def diverges(): Boolean = agent.diverges()
  
  override
  def hashCode() = {
    sxmash(19, (19, agent.hashCode()))
  }
  
  override
  def equals(rhs: Any) = {
    rhs match {
      case ag: PRestrict => ag.agent == agent && ag.restriction == restriction
      case _ => false
    }
  }
  
}

case class PRelabel(agent: CCSAgent, relabel: Relabeling) extends PrivateAgent{
  def agentString = {
    agent.privAgent match {
      case v: PVar => agent.agentString + relabel.relabellingString
      case n: PNil => agent.agentString + relabel.relabellingString
      case _ => "(" + agent.agentString + ")" + relabel.relabellingString
    }
  }
  def diverges(): Boolean = agent.diverges()

  override
  def hashCode = sxmash(77, (agent.hashCode(), relabel.hashCode()))
  
  override
  def equals(rhs: Any) = {
    rhs match {
      case ag: PRelabel => {
        val relAg = ag.asInstanceOf[PRelabel]
        agent == relAg.agent && relabel == relAg.relabel
      }
      case _ => false
    }
  }
}


object PrivateAgent {
  // Prints a list of agents separated with the given delimiter.
  def agentListString(agents: List[CCSAgent], delim: String): String = {
    var string = ""
    for (i <- 0 until agents.length) {
      var agent = agents(i)
      agent.privAgent match {
       case ag: PSSum => string += "(" + ag.agentString + ")"
       case ag: PParallel => string += "(" + ag.agentString + ")"
       case ag => string += ag.agentString
      }
      if (i != agents.length -1) string += delim
    }
    
    
    agents match {
        case Nil => ""
        case curr :: List() => curr.agentString
        case curr :: list => curr.agentString + delim + agentListString(list, delim)
      }
  }
}
